Add more support to mir fn bodies #197
Conversation
| #[grammar(struct {$,v0} as $v1)] | ||
| Struct(Vec<ValueExpression>, Ty), |
There was a problem hiding this comment.
In minirust, struct is represented as a tuple:
/// An n-tuple, used for arrays, structs, tuples (including unit).
Tuple(List<ValueExpr>, Type),
I'd prefer not grouping arrays, structs and tuples together in one enum variant, because struct is an adt in rustc, and others are not (although it is technically possible to represent all of them as adt?). It'd be quite bad to do typechecking for both adt and non-adt together.
crates/formality-prove/src/decls.rs
Outdated
| #[term($:where $,where_clause { $,variants })] | ||
| pub struct AdtDeclBoundData { | ||
| /// The where-clauses declared on the ADT, | ||
| pub where_clause: Wcs, | ||
| pub variants: Vec<AdtDeclVariant>, | ||
| } | ||
|
|
||
| #[term($name { $,fields })] | ||
| pub struct AdtDeclVariant { | ||
| pub name: VariantId, | ||
| pub fields: Vec<AdtDeclField>, | ||
| } | ||
|
|
||
| #[term($name : $ty)] | ||
| pub struct AdtDeclField { | ||
| pub name: AdtDeclFieldName, | ||
| pub ty: Ty, | ||
| } | ||
|
|
||
| #[term] | ||
| pub enum AdtDeclFieldName { | ||
| #[cast] | ||
| Id(FieldId), | ||
| #[cast] | ||
| Index(usize), | ||
| } |
There was a problem hiding this comment.
I also added the variant information to AdtDeclBoundData because I find it a lot nicer to get struct field type information directly from decl in bffdf5a#diff-be3230c387ee7e1ccef3d2eea52917c384f3bf0f656bcdb10e1f28bf3dcfdb5b.
| bail!( | ||
| "PlaceExpression::Local: unknown local name `{:?}`", | ||
| local_id | ||
| ) | ||
| }; | ||
| place_ty = ty; | ||
| } | ||
| Field(field_projection) => { | ||
| let Local(ref local_id) = *field_projection.root else { |
There was a problem hiding this comment.
we can recursively invoke check_place(&field_projection.root), no?
| bail!("The local id used in PlaceExpression::Field is invalid.") | ||
| }; | ||
|
|
||
| let Some(adt_id) = ty.get_adt_id() else { |
There was a problem hiding this comment.
right now we are checking for ADTs, but eventually we will want to do normalization here -- so probably this check_place function should become a judgment at that time
| bail!("The type used in ValueExpression::Struct must be adt") | ||
| }; | ||
|
|
||
| // Check the validity of the struct. |
There was a problem hiding this comment.
we probably want to "prove ty is well-formed" somewhere in here
| bail!("This type used in ValueExpression::Struct should be a struct") | ||
| } | ||
|
|
||
| let struct_field_ty: Vec<Ty> = |
There was a problem hiding this comment.
| let struct_field_ty: Vec<Ty> = | |
| let struct_field_tys: Vec<Ty> = |
| let ty = self.check_value(typeck_env, value_expression)?; | ||
|
|
||
| // Make sure the type matches the declared adt. | ||
| if ty != declared_ty { |
There was a problem hiding this comment.
this should prove a subtype relation
There was a problem hiding this comment.
what you could do is use Wcs::all_sub from that other branch we were working on and prove all of them at once; this would be nice
This PR supports: